This is a quick implementation of the idea we had a long time ago for exporting our protected invariants into YAML witnesses with ghosts.

protection privatization

For the Freiburg mutex.c example, we essentially generate the same witness with ghosts as the example:

• A ghost variable m_locked is declared and updated to match lock and unlock operations of the mutex m.
• A flow-insensitive invariant used == 0 || m_locked is generated using the ghost variable.

This is still our special flow_insensitive_invariant because there's the question where one would place the location_invariant when our result in fact holds at every point.

Currently tested only manually with:

./goblint ~/Documents/concurrency-witnesses/examples/VEWIT2023/mutex.c --enable ana.sv-comp.functions --set pre.cppflags[+] "-DGOBLINT_NO_PTHREAD_ONCE" --html --set ana.activated[+] mutexGhosts --enable witness.yaml.enabled --set witness.yaml.entry-types[+] flow_insensitive_invariant

mutex-meet privatization

For this example, the result is the same, but one invariant is generated per-mutex with a conjunction for all the protected variables. Also for the relational privatization.

TODO

• Add tests using Add cram tests for YAML witnesses #1357.
• Clean ghost variable management up to not be string-based.
• What is the right invariant for multiple protecting mutexes?
• What to do about ambiguous/unknown mutex lock and unlock operations? When do we have to generate a ghost update to which ghost variable?
  • Detect ambiguity and give up on those mutexes and globals.
• Valid C names for ghost variables, in particular for (alloc@...) locks.
• Add ghost variable for multi-threaded mode to avoid needing earlyglobs.
• Prune unused ghost variables.
• Are mutex-meet multiple-protecting invariants even right?
• Adapt ghost update locations to Change YAML witness columns to 1-indexed #1400.
• Unlock updates are on wrong node (but lock updates are right)?
• e235ba7 broke OSX only
• Options to disable ghost_variable and ghost_update entry types.
• Relational mutex-meet.
• Option to output __VERIFIER_atomic invariants unconditionally: they should not be observable anyway, but those ghost updates can be technically tricky to work with.